T:Type, L1, L2, L3:T List. L1  L2  L2 || L3  L1 || L3 

latex

Definitions	t  T, x:A. B(x), l1 || l2, P  Q, x:A. B(x), as @ bs, Prop, l1  l2
Lemmas	append wf, compat-append, append nil sq, compat wf